\documentclass{article}
\usepackage{xcolor} 
\usepackage{fullpage} 
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{proof}
\usepackage{hyperref}
\usepackage{caption}
\usepackage{comment}
\usepackage{subcaption}
\usepackage{fancybox}
\usepackage{stmaryrd}
\pagestyle{plain}

\begin{document}
\title{Type Inference Review}

\author{Peng Fu}
\date{\today}




%% The extension include: 
%% 1. polymorphic recursion.
%%     It is semi-decidable, see 
%%       Mycroft, Polymorphic type schemes and recursive definitions. 
%%     Haskell support this through explicit annotation.. 

%% 2. Higher rank polymorphism(I particularly like Mark Jones' First-class Polymorphism with Type Inference; also, SPJ and company's Boxy types: type inference for higher-rank types and impredicativity). 

%% 3. type class. (one can cite Wadler and Blott's paper, my personal favorite is 
%% again, Mark Jones' PhD thesis: Quanlified Types: theory and practice)

%% 4. GADT and type family(I am not a fan, but SPJ and company is writing 
%% a journal called Modular type inference with local assumptions, which basically summarize Haskell's way to deal with 1-4.) 


\maketitle

HM type inference is widely adopted in many mordern functional programming languages. There
are several reasons that contributed to its success: 1. Type inference is decidable at compile time. 2. Programmer does not need to annotate their programs\footnote{Although data type declaration is a form of annotation, but other than this, all the other programs can be annotation free.}. 3. Each typable program has a unique most general type (principal type). While it is desirable to preserve property 1-3, some extensions makes certain compromises on 1-3, but gains extra expressiveness\footnote{Here expressiveness means allowing more meaningful programs to be typable compare to HM.} and flexibility. We will discuss four orthogonal extensions of HM type inference. 

\textit{Polymorphic recursion} When type check a recursive definition, there is a question of wether all the recursive occurence should have the same type. HM type inference simply insists all the recursive occurrence have the same type, while it has the virtue of simplicity, this restriction does prevent a range of meaningful programs to be typable. A. Mycroft \cite{Mycroft:1984} propose an inference algorithm that extend HM to support polymorhpic recursive occurrence. However, it has been show that this extension is undecidable (\cite{Henglein:1993}, \cite{Kfoury:1993}). In practice, explicit type annotation is needed to make type inference decidable \cite{Pottier}.       

\textit{First class polymorphism} In the question of how to support System \textbf{F} polymorphism, Mark Jones \cite{Jones:1997} proposed an decidable extension of HM where the only annotation needed is in the declaration of data type constructors, which is very moderated considering we are already commited to annotate the data type constructors. There are other approach to first class polymorphism through annotations on other different places (an incomplete list: \cite{Odersky:1996}, \cite{PeytonJones:2007}, \cite{Leijen:2009}).

\textit{Type class} First appeared in Wadler and Blott \cite{Wadler:1989}, type class is intended to support operator overloading through resolving instances and programs transformation, so in principle, type class can be reduced to a language with only data type and pattern matching. The type inference with type class in general is considerd decidable\footnote{w.r.t. the decidability of instance resolution.} and every typable program has a principal type \cite{jones2003qualified}. Annotations are only needed in the class declaration, which will be translated to data type declaration \cite{Wadler:1989}. In concrete implementation, several design decisions needed to be made \cite{jones1997type}. Historically, M. Jones's Gofer \cite{jones2003qualified} supports a much more liberal and expressive type class compared to Haskell. Since the invention of type class, it founds many applications, e.g. monad type class, which made imperative programming more accessible in a pure functional language \cite{PeytonJones:1993}.

\textit{Generalized algebraic data type} GADT provides a form of equality constraints on types 
when defining data type constructor. It is first introduced into functional programming language in a draft by Lennart Augustsson and Kent Petersson under the title ``Silly Type Families'', then after 9 years, several researchers independently re-introduced the similar ideas(an incomplete list: \cite{cheney2003first}, \cite{Xi:2003}, \cite{Sheard:2004}). Without explicit annotating the programs, it is well-known that type inference for GADT does not exibit principal type \cite{Vytiniotis:2011}. Given full annotation, type inference for GADT becomes decidable (\cite{cheney2003first}, \cite{Simonet:2007}). A comprehensive survey related works on GADT can be found in \cite{Vytiniotis:2011}.  




\bibliographystyle{plain}

\bibliography{review}

\end{document}
